TIMEOUT

We are left with following problem, upon which TcT provides the
certificate TIMEOUT.

Strict Trs:
  { <(x, y) -> #cklt(#compare(x, y))
  , merge(nil(), ys) -> ys
  , merge(::(x, xs), nil()) -> ::(x, xs)
  , merge(::(x, xs), ::(y, ys)) -> ifmerge(<(x, y), x, xs, y, ys)
  , ifmerge(true(), x, xs, y, ys) -> ::(x, merge(xs, ::(y, ys)))
  , ifmerge(false(), x, xs, y, ys) -> ::(y, merge(::(x, xs), ys))
  , msplit(nil()) -> pair(nil(), nil())
  , msplit(::(x, nil())) -> pair(::(x, nil()), nil())
  , msplit(::(x, ::(y, ys))) -> msplit'(x, y, msplit(ys))
  , msplit'(x, y, pair(xs, ys)) -> pair(::(x, xs), ::(y, ys))
  , mergesort(nil()) -> nil()
  , mergesort(::(x, nil())) -> ::(x, nil())
  , mergesort(::(x, ::(y, ys))) ->
    mergesort'(msplit(::(x, ::(y, ys))))
  , mergesort'(pair(xs, ys)) -> merge(mergesort(xs), mergesort(ys)) }
Weak Trs:
  { #compare(#0(), #0()) -> #EQ()
  , #compare(#0(), #neg(y)) -> #GT()
  , #compare(#0(), #pos(y)) -> #LT()
  , #compare(#0(), #s(y)) -> #LT()
  , #compare(#neg(x), #0()) -> #LT()
  , #compare(#neg(x), #neg(y)) -> #compare(y, x)
  , #compare(#neg(x), #pos(y)) -> #LT()
  , #compare(#pos(x), #0()) -> #GT()
  , #compare(#pos(x), #neg(y)) -> #GT()
  , #compare(#pos(x), #pos(y)) -> #compare(x, y)
  , #compare(#s(x), #0()) -> #GT()
  , #compare(#s(x), #s(y)) -> #compare(x, y)
  , #cklt(#EQ()) -> #false()
  , #cklt(#GT()) -> #false()
  , #cklt(#LT()) -> true() }
Obligation:
  runtime complexity
Answer:
  TIMEOUT

Computation stopped due to timeout after 300.0 seconds.

Arrrr..